es:ES, i:Id, ds:x:Id fp Type. @i discrete ds  (discrete state@i r State(ds)) 

latex

Definitions	ff, tt, if b then t else f fi , x,y. t(x;y), , x. t(x), t  T, f(x)?z, Top, State(ds), discrete state@i, @i discrete ds, P  Q, x:A. B(x), P  Q, Unit, , False, A, P & Q, x(s1,s2), x(s), @i(x:T), xdom(f). v=f(x)   P(x;v),
Lemmas	assert of bnot, eqff to assert, iff transitivity, eqtt to assert, not wf, bnot wf, bool wf, event system wf, fpf wf, fpf-trivial-subtype-top, fpf-dom wf, assert wf, es-dtype wf, id-deq wf, Id wf, fpf-all wf, subtype rel self, fpf-cap wf, top wf, es-vartype wf, es-isconst wf, ifthenelse wf, subtype rel dep function